Nuprl Definition : msg-spec-join
11,40
postcript
pdf
a
b
==
a
b
latex
clarification:
a
b
== fpf-join(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
a
;
b
)
latex
Definitions
f
g
,
product-deq(
A
;
B
;
a
;
b
)
,
Knd
,
IdLnk
,
KindDeq
,
IdLnkDeq
FDL editor aliases
msg-spec-join
origin
b == a b
b == fpf-join(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);a;b) b == a b
b == fpf-join(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);a;b) g